XB: Convergent Replicated Datatypes in Lean
Lean is a modern, general-purpose programming language featuring advanced functional programming constructs such as pattern matching, recursion, immutable datastructures, type classes, dependent types and more. At the same time, Lean compiles to C++, featuring easy interopability with low-level libraries where necessary.
A Conflict-free Replicated Data Type (CRDT) are an abstraction and design pattern for multi-user applications. CRDTs are decentralized: they do not assume the use of a single server, so they can be used in peer-to-peer networks and other decentralised settings. For this the CRDT interface requires an initial state and a merge function for any two states, to ensure that whenever different users made different edits, the end result can be merged together.
Your task will be to write CRDTs in the Lean programming language and verify that they have the necessary properties CRDTs need.